1. Technical Field
The present disclosure relates to a timing analysis method for a circuit, in particular, to a functional timing analysis method for circuit timing verification.
2. Description of Related Art
In modern synthesis flow of very large scale integration (VLSI) system design, timing analysis is essential in identifying timing critical regions for re-synthesis, determining operable clock frequencies, and avoiding wasteful over-optimization and thus accelerating design closure in meeting stringent timing constraints. Since timing analysis has to be performed repeatedly during circuit design, the complex computation of timing analysis may cause serious overhead in the design process.
There are two main methods to timing analysis for a circuit, wherein one is a static timing analysis method, and the other one is a functional timing analysis method. The static timing analysis method, based on pure structural (or topological) analysis, through fast with linear-time complexity, can be too pessimistic in estimating circuit delay due to the ignorance of false or non-sensitizable paths of the circuit. On the other hand, the functional timing analysis method provides accurate delay calculation, but is computationally intractable, i.e. an NP-hard problem, in identifying false critical paths.
A timed characteristic function of a node in the circuit is used in the functional timing analysis method to characterize the set of input assignments to the circuit that make the output value of the node change from the initial unknown value to a final stabilized value and meet a specified timing requirement.
The conventional functional timing analysis method uses equation-based conversion to translate a complex timed characteristic function associated with a selected delay time into a conjunctive normal form formula for satisfiability solving. The conventional functional timing analysis method may use the Boolean satisfiability solver to check whether the conjunctive normal form formula is satisfiable.
If the conjunctive normal form formula is satisfiable, the selected delay time of the node is attainable (that is, there exists some input assignment whose signal propagation makes the node stabilize to its final value meeting the specified delay time constraint). Otherwise, the selected delay time of the node is not attainable (that is, there exists no input assignment whose signal propagation makes the node stabilize to its final value meeting the specified delay time constraint).
The conventional functional timing analysis method produces complex formulas making satisfiability solving inefficient. Therefore, the conventional functional timing analysis method is hardly applicable to analyzing complex designs.